T:Type, R:(TTType). SWellFounded(R(x,y))  wellfounded{i:l}(T; x,y.R(x,y)) 

latex

Definitions	x:A. B(x), P  Q, SWellFounded(R(x;y)), x(s1,s2), wellfounded{i:l}(A; x,y.R(x;y)), x:A. B(x), prop{i:l}, x(s), guard(T), t  T, ge(i; j), A  B, A, False, , T, True
Lemmas	nat wf, nat properties, ge wf, le wf